/-- 递归读取用户输入，直到遇到空行为止 -/
partial def getLines : IO String := do
  IO.print "Enter your text: "
  let line ← (← IO.getStdin).getLine
  if line.trim.isEmpty then
    return line.trimRight
  else
    return line.trimRight ++ (← getLines)

/-- 主程序：读取并拼接多行输入 -/
def main : IO Unit := do
  let stdin ← getLines
  IO.println s!"Concatenated lines: {stdin}"-- 
  
-- def name : String := "Rex"
-- def main : IO Unit := IO.println s!"Hello, {name}!"